Added character functions to API #5549

CEisenhofer · 2021-09-15T06:42:24Z

No description provided.

NikolajBjorner · 2021-09-15T08:02:04Z

src/api/c++/z3++.h

@@ -1445,6 +1445,31 @@ namespace z3 {
            check_error();
            return expr(ctx(), r);
        }
+        expr charle() const {


Naming conventions elsewhere:
char_le
char_to_int
char_to_bv
...

NikolajBjorner · 2021-09-15T08:03:45Z

src/ast/char_decl_plugin.cpp

@@ -90,7 +90,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
        else if (!b.is_bv_sort(domain[0]) || b.get_bv_size(domain[0]) != num_bits())
            msg << "expected bit-vector sort argument with " << num_bits();
        else {
-            m.mk_func_decl(symbol("char.to_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr));
+            return m.mk_func_decl(symbol("char.from_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr));


NikolajBjorner · 2021-09-15T08:05:04Z

/usr/bin/clang++ -DJULIA_ENABLE_THREADING -Dz3jl_EXPORTS -I/home/vsts/work/1/s/src/api -I/home/vsts/work/1/s/build/src/api -I/home/vsts/work/1/s/src/api/c++ -isystem /home/vsts/.julia/artifacts/b55cd96f4dd60da926644fc18aef04c69f891b7d/include -isystem /usr/local/julia1.6.2/include/julia -Werror=odr  -Werror=delete-non-virtual-dtor  -Werror=overloaded-virtual  -fcolor-diagnostics -O2 -g -DNDEBUG -fPIC -std=gnu++17 -MD -MT src/api/julia/CMakeFiles/z3jl.dir/z3jl.cpp.o -MF src/api/julia/CMakeFiles/z3jl.dir/z3jl.cpp.o.d -o src/api/julia/CMakeFiles/z3jl.dir/z3jl.cpp.o -c /home/vsts/work/1/s/src/api/julia/z3jl.cpp
In file included from /home/vsts/work/1/s/src/api/julia/z3jl.cpp:2:
/home/vsts/work/1/s/src/api/c++/z3++.h:1449:24: error: no matching function for call to 'Z3_mk_char_le'
            Z3_ast r = Z3_mk_char_le(ctx(), *this);
                       ^~~~~~~~~~~~~
/home/vsts/work/1/s/src/api/z3_api.h:3794:19: note: candidate function not viable: requires 3 arguments, but 2 were provided
    Z3_ast Z3_API Z3_mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2);
                  ^
1 error generated.

Added character functions to API

6c190f0

NikolajBjorner reviewed Sep 15, 2021

View reviewed changes

Changed names of c++ functions

f324d3c

NikolajBjorner merged commit c58b2f4 into Z3Prover:master Sep 15, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added character functions to API #5549

Added character functions to API #5549

CEisenhofer commented Sep 15, 2021

NikolajBjorner Sep 15, 2021

NikolajBjorner Sep 15, 2021

NikolajBjorner commented Sep 15, 2021

Added character functions to API #5549

Added character functions to API #5549

Conversation

CEisenhofer commented Sep 15, 2021

NikolajBjorner Sep 15, 2021

Choose a reason for hiding this comment

NikolajBjorner Sep 15, 2021

Choose a reason for hiding this comment

NikolajBjorner commented Sep 15, 2021